\begin{tabbing}
ecl{-}mng{-}sends\=\{i:l\}\+
\\[0ex](${\it es}$; $i$; ${\it ds}$; ${\it da}$; $x$; $l$; ${\it snd}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=es{-}decls(${\it es}$;$i$;${\it ds}$;${\it da}$)\+
\\[0ex]$\Rightarrow$ es{-}sends{-}iff(${\it es}$;$l$;ecl{-}tags($l$;${\it snd}$);${\it da}$;${\it ds}$;$e$.tagged{-}list{-}messages(\=es{-}state{-}when(${\it es}$;$e$);\+
\\[0ex]es{-}val(${\it es}$; $e$);
\\[0ex]mapfilter(\=$\lambda$${\it tr}$.\+
\\[0ex]$\langle$1of(${\it tr}$)
\\[0ex]$,\,$\=2of(2of(\+
\\[0ex]${\it tr}$))$\rangle$;
\-\\[0ex]$\lambda$${\it tr}$.
\\[0ex]es{-}bact\=\{i:l\}\+
\\[0ex](\=${\it ds}$;\+
\\[0ex]${\it da}$;
\\[0ex]$x$;
\\[0ex]${\it es}$;
\\[0ex]1of(
\\[0ex]2of(
\\[0ex]${\it tr}$));
\\[0ex]es{-}init(${\it es}$;$e$);
\\[0ex]$e$
\\[0ex]);
\-\-\\[0ex]fpf{-}cap(${\it snd}$;product{-}deq(Knd;IdLnk;KindDeq;IdLnkDeq);\=$\langle$\=es{-}kind\+\+
\\[0ex](\=${\it es}$;\+
\\[0ex]$e$
\\[0ex])
\-\-\\[0ex]$,\,$$l$$\rangle$;nil))))
\-\-\-\-
\end{tabbing}